Nuprl Lemma : ma-single-bframe_wf 11,40
k:Knd, L:(IdLnk List). k sends only on links in L  MsgA 
latex

DefinitionsId, t  T, Knd, type List, x.A(x), x. t(x), x:A. B(x), , IdLnk, x : v, x:A  B(x), Void, Type, Top, x:AB(x), State(ds), , mk-ma, k sends only on links in L, MsgA
Lemmasmk-ma wf, ma-state wf, top wf, fpf-single wf, IdLnk wf, fpf-empty wf, Knd wf, Id wf

origin